Electronic circuits are used in a variety of products, from automobiles to microwaves to personal computers. Designing and fabricating electronic circuits and devices that encompass these circuits typically involves many steps, sometimes referred to as the “design flow.” The particular steps of a design flow often are dependent upon the type of electronic circuit, its complexity, the design team, and the electronic circuit fabricator or foundry that will manufacture the circuit. Typically, software and hardware “tools” verify the design at various stages of the design flow by running software simulators and/or hardware emulators. These steps aid in the discovery of errors in the design, and allow the designers and engineers to correct or otherwise improve the design.
Several steps are common to most design flows. Initially, a specification describing the desired functionally for a new circuit is generated. Subsequently, the specification is transformed into a logical design, sometimes referred to as a register transfer level (RTL) description of the circuit. With this logical design, the circuit is described in terms of both the exchange of signals between hardware registers and the logical operations that are performed on those signals. The logical design is typically embodied in a Hardware Design Language (HDL), such as the Very high speed integrated circuit Hardware Design Language (VHDL). At this point, the logic of the circuit is often analyzed, to confirm that it will accurately perform the functions described in the specification. This analysis is sometimes referred to as “functional verification.”
After the accuracy of the logical design is confirmed, it is converted into a device design by synthesis software. The device design, which is typically in the form of a schematic or netlist, describes the specific electronic devices (such as transistors, resistors, and capacitors) that will be used in the circuit, along with their interconnections. This device design generally corresponds to the level of representation displayed in conventional circuit diagrams and is often referred to as a “gate-level” design. The relationships between the electronic devices specified by the gate-level design are then analyzed, often mathematically, to confirm that the circuit described by the gate-level design corresponds to the circuit described by the register transfer level design. This analysis is typically referred to as “formal verification.”
Once the components and their interconnections are established, the design is again transformed, this time into a physical design that describes specific geometric elements. This type of design often is referred to as a “layout” design. The geometric elements, which typically are polygons, define the shapes that will be created in various layers of material to manufacture the circuit. Lines are then routed between the geometric elements, which will form the wiring used to interconnect the geometric components and form the electronic devices specified by the gate-level design. After the layout design is completed, the design can be manufactured into a circuit via an appropriate manufacturing process, such as, for example, an optical lithographic process.
As indicated, verification processes often take place after a “higher-level” design has been synthesized into a “lower-level” design, such as, for example, synthesizing a gate-level design from a register transfer level design. These verification processes seek to ensure that the synthesized design is logically equivalent to the design from which it was synthesized. In the case of formal verification, mathematical theorems are used to determine if the two designs are logically equivalent. However, some operations carried out during synthesis, such as, for example, retiming operations, may cause conventional formal verification methods to fail even where the two designs are logically equivalent. This is due to the fact that, in order to determine logical equivalence, conventional formal verification techniques rely on the structural similarity of the two designs. As such, where structural transformations are made to a design during synthesis, conventional techniques are insufficient to formally verify these designs. As those of skill in the art will appreciate, modern synthesis processes often include structural transformation operations. In many cases, the structural transformation operations, such as, for example, retiming, are done to meet design or manufacturing constraints. Some example of structural transformation techniques are, retiming, state minimization, state encoding, sequential-redundancy removal, redundancy removal and addition.
One proposed technique to formally verify structurally transformed designs is referred to as sequential equivalence checking, which is discussed in detail in Principles of Sequential-Equivalence Verification, by Maher N. Mneimneh and Karem A. Sakallah, Design and Test of Computers, pp. 248-257, vol. 22, issue 3, 2005, which article is incorporated entirely herein by reference. As those of skill in the art will appreciate, sequential equivalence checking requires traversing the state space of the two designs prior to verification. As such, sequential equivalence checking techniques require significantly more computational resources than conventional formal verification techniques require. Furthermore, the state space of the design must be traversed during sequential equivalence checking. As those of skill in the art will appreciate, the state space increases exponentially with the size of the circuit design. As a result, it is often not feasible to formally verify a design using sequential techniques due to the size of the state space.